The generated code now uses implicit type and const generic parameters.

For instance, the following code:

pub fn choose<'a, T>(b: bool, x: &'a mut T, y: &'a mut T) -> &'a mut T {
    if b {
        x
    } else {
        y
    }
}

now extracts to (the type T is now implicit):

def choose
  {T : Type} (b : Bool) (x : T) (y : T) :
  Result (T × (T → Result (T × T)))
  :=
  if b
  then let back := fun ret => Result.ok (ret, y)
       Result.ok (x, back)
  else let back := fun ret => Result.ok (x, ret)
       Result.ok (y, back)

The rule we are using is that any type or const generic parameter is implicit if it is referred by the trait clauses or the input values. Importantly, we ignore the output value. This means that the type parameter in Vec::new is still explicit, because it can't be inferred from the inputs:

def Vec.new (α : Type u): Vec α := ...